-----------------------------------------------------------------------------
--
-- Module      :  Data.TypeLevel.Boolean
-- Copyright   :
-- License     :  AllRightsReserved
--
-- Maintainer  :  eduard.sergeev@gmail.com
-- Stability   :  Highly Experimental
-- Portability :
--
-- Type-level booleans
--
-----------------------------------------------------------------------------

{-# LANGUAGE NoImplicitPrelude, TypeFamilies, TypeOperators, UndecidableInstances #-}

module Data.TypeLevel.Boolean (

   Boolean,
   True,
   False,

   And,
   Or,
   Not,

) where

import Data.TypeLevel.Families
import Prelude (Show(show))

-- * Type-level booleans
-- | Type-level data type definition
class Boolean b
instance Boolean True
instance Boolean False

-- | Type-level data constructor True 
data True
-- | Type-level data constructor False 
data False


-- * Logical AND
type family And l r :: *
type instance And l r = l :*: r

type instance False :*: r = False
type instance True :*: r = r
{-
type instance True :*: True = True
type instance True :*: False = False
type instance False :*: True = False
type instance False :*: False = False
-}

-- * Logical OR
type family Or l r :: *
type instance Or l r = l :+: r

type instance True :+: r = True
type instance False :+: r = r
{-
type instance False :+: False = False
type instance True :+: False = True
type instance False :+: True = True
type instance True :+: True = True
-}

-- * Logical NOT
type family Not b :: *
type instance Not True = False
type instance Not False = True


instance Show True where
    show _ = "True"

instance Show False where
    show _ = "False"
